{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Spot"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 16,
   "metadata": {},
   "outputs": [],
   "source": [
    "from ml2.tools.spot import Spot"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "INFO:ml2.tools.containerized_grpc_service:Spot container happy_solomon on port 50051 is running\n",
      "INFO:ml2.tools.containerized_grpc_service:Successfully connected to Spot gRPC server running in container happy_solomon on port 50051\n"
     ]
    }
   ],
   "source": [
    "spot = Spot()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "(<LTLSatStatus.SATISFIABLE: 'satisfiable'>, 'a & b; cycle{1}')"
      ]
     },
     "execution_count": 18,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "spot.check_sat('F a & F b')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 19,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "<TraceMCStatus.SATISFIED: 'satisfied'>"
      ]
     },
     "execution_count": 19,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "spot.mc_trace('F a & F b', 'a & b; cycle{1}')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 20,
   "metadata": {},
   "outputs": [
    {
     "name": "stderr",
     "output_type": "stream",
     "text": [
      "INFO:ml2.tools.containerized_grpc_service:Stopped and removed container happy_solomon running Spot on port 50051\n"
     ]
    }
   ],
   "source": [
    "del spot"
   ]
  }
 ],
 "metadata": {
  "interpreter": {
   "hash": "8caa4319d59a734f94e739df6b594acde678ec5f2e3eb7152d087fc4a1992669"
  },
  "kernelspec": {
   "display_name": "Python 3.7.3 64-bit ('ml2': pyenv)",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.8.12"
  },
  "orig_nbformat": 2
 },
 "nbformat": 4,
 "nbformat_minor": 2
}
